Applications of existing logical planning methods mostly rely on purely discrete abstractions of robotic behaviors. We are extending linear logic to incorporate constraints drawn from possibly continuous domains for which tractable solvers exist. The resulting language, CILL(Constrained Intuitionistic Linear Logic), is capable of natively representing hybrid aspects of robot behaviors, providing a sound and complete mechanism for automatically synthesizing provably correct plans to achieve user-specified goals. Intuitionistic linear logic, due to its rejection of the structural rules of contraction and weakening, allows us to treat hypotheses as consumable resources and approximate temporal progress through a logical proof. In order to easily experiment with different encodings of robotic planning problems within CILL, we are using SWI-Prolog to construct an unoptimized but usable backwards theorem prover for Constrained Intuitionistic Linear Logic. In order to make nontrivial proof search feasible, we are incorporating focusing and resource management schemes from the literature into this system.

DATE: 15 December, 2008, Monday@ 16:20
PLACE: EA 409